package useless;

import formula.BinaryFormula;
import proof.Proof;
import proof.ProofRule;
import proof.DerivedProof;
import sign.FormulaSign;

import java.util.ArrayList;
import java.util.Set;

public class Solution {
    /*
    public static Proof Separation(ArrayList<Proof> conditions){
        //从conditions中过滤出全部的ANY,EXIST，并创建出新ArrayList,然后添加
//        ArrayList<Proof> anyList=new ArrayList<>();
//        ArrayList<Proof> existList=new ArrayList<>();
//        for (Proof condition:conditions) {
//            BinaryFormula bf=(BinaryFormula) condition.getConclusion();
//            if (bf.getSign()== FormulaSign.ANY){
//                anyList.add(condition);
//            }else {
//                existList.add(condition);
//            }
//        }




//        while(true){//检验是否生成了所有new formula
//            //第二轮以及之后，existList=new_ex_f,同时更新totalExist
//            ArrayList<Proof> testing_arr=new useless.Solution().fun(anyList,);
//        }do {
//            ArrayList<Proof> testing_arr=new useless.Solution().fun(anyList,existList,new HashSet<>(existList));//第一轮，totalExist=existList
//
//        }
        return null;
    }

     */

    //从conditions中过滤出全部的ANY,EXIST，并创建出新ArrayList,然后添加
    public ArrayList<Proof> Separate_ANY(ArrayList<Proof> conditions){
        ArrayList<Proof> anyList=new ArrayList<>();
        for (Proof condition:conditions) {
            BinaryFormula bf=(BinaryFormula) condition.getConclusion();
            if (bf.getSign()== FormulaSign.ANY){
                anyList.add(condition);
            }
        }
        return anyList;
    }

    public ArrayList<Proof> Separate_EXIST(ArrayList<Proof> conditions){
        ArrayList<Proof> existList=new ArrayList<>();
        for (Proof condition:conditions) {
            BinaryFormula bf=(BinaryFormula) condition.getConclusion();
            if (bf.getSign()== FormulaSign.EXIST){
                existList.add(condition);
            }
        }
        return existList;
    }


    //遍历，生成新formula；检查新formula是否存在于totalExist中，不存在就返回一个新的new_ex_f
    public Set<Proof> fun(ArrayList<Proof> anyList, ArrayList<Proof> existList, Set<Proof> totalExist){
        int before_size=totalExist.size();
        ArrayList<Proof> new_ex_f=new ArrayList<>();
        for (Proof any:anyList) {
            for (Proof exist:existList) {//generate new D1 formula
                ArrayList<Proof> ps = new ArrayList<>();
                ps.add(any);
                ps.add(exist);
                if (ProofRule.D1.applyRule(ps) != null){
                    //判断是否出现重复的Exist
                    if (totalExist.contains(new DerivedProof(ps,ProofRule.D1))){
                        continue;
                    }else {
                        new_ex_f.add(new DerivedProof(ps,ProofRule.D1));
                        totalExist.add(new DerivedProof(ps,ProofRule.D1));
                    }
                }
            }
        }
        int after_size=totalExist.size();
        if (before_size!=after_size){//说明有new formula生成，继续递归
            return fun(anyList, new_ex_f, totalExist);
        }else {//没有new formula生成，所有formula都被生成，递归结束
            return totalExist;
        }

    }


}
